package systemf



trait SystemFDesugar extends Desugar{
  //used to convert to form with debruijn indices
  

  override type RawTerm = LTerm
  type CleanTerm = LTerm
  type RawType = LType
  type CleanType = LType
  
  def desugar(t: RawTerm):CleanTerm= desugar_(new Context(Nil))( t)
  def desugar(ty:RawType):CleanType= desugarty(new Context(Nil))(ty)
  
  def desugarty(ctx:Context)(ty: RawType) :CleanType = ty match {
  case base:BaseType      => base

  case TyVarName(str)     => {
    val i = ctx getIndexOfName str 
    TyVar(i)
  }
  case r@TyArr(ty1:RawType,ty2:RawType)     => {
    r.map(desugarty(ctx))
  }
  case TyUniversal(TyVarName(x), ty:RawType)      => {
    val ctx2 = ctx + (x, TypeVarBinding(x)) //CAREFUL: don't forget to bind the var, we will need to look up indices in the body
    val ty_ = desugarty(ctx2) (ty)
    TyUniv(x, ty_)
  }
  case TyExistential(TyVarName(x), ty:RawType)     => {
    val ctx2 = ctx + (x, TypeVarBinding(x))
    val ty_ = desugarty(ctx2) (ty)
    TyExist(x, ty_)
  }
  case r@TyRecord(fields:List[(String, RawType)])   => {
    TyRecord(r.map(desugarty(ctx)))
  }
  }
  
  
  def desugar_(ctx:Context)(t: RawTerm):CleanTerm = t match {
    case ty: LType           => throw new Exception("desugaring: taking lterm branch when should be taking ltype branch")
    case base:BaseValue      => base
    case Lambda(n,ty:RawTerm,t:RawTerm) => n match { case VarName(str) => {
      val ty2:CleanType = desugarty(ctx) (ty)         //CAREFUL: do the type in the outer scope, not in the inner one
      val ctx2 = ctx + (str, VarBinding(ty2))
      
      val t2 = desugar_ (ctx2) (t) // Q: interpret: discarding resulting ctx
      Lam(str,ty2,t2) //
    }}
    case TyLambda(n,t:RawTerm) => n match { case TyVarName(str) => {
      val ctx2 = ctx + (str, TypeVarBinding(str))
      val t2 = desugar_(ctx2) (t)
      TLam(str, t2)
    }}
    case VarName(str) =>  {
      val i = ctx getIndexOfName str 
      Var(i)
    }

    case Applic(t1:RawTerm,t2:RawTerm)         => 
      val t1_ = desugar_(ctx)( t1)
      val t2_ = desugar_(ctx)( t2)
      App(t1_,t2_)
    case TyApplic(t:RawTerm,ty:RawTerm)        =>
      val t_ = desugar_(ctx) (t)
      val ty_ = desugarty(ctx) (ty)
      TApp(t_,ty_)
      
    case Let(VarName(str),t1:RawTerm,t2:RawTerm) =>
      val ctx2 = ctx + (str, NameBinding(str))
      val t1_ = desugar_(ctx) (t1)
      val t2_ = desugar_(ctx2) (t2)
      Let(VarName(str),t1_,t2_)
      
    case RecProj(t1:RawTerm,label)      => 
      val t1_ = desugar_(ctx) (t1)
      RecProj(t1_,label)
    case r@Record(fields:List[(String,LTerm with RawTerm)])       => {
      Record(r.map(desugar_(ctx)))

    }
    
    

    case If(c:RawTerm,p:RawTerm,n:RawTerm) => {
      val c2 = desugar_(ctx) (c)
      val p2 = desugar_(ctx) (p)
      val n2 = desugar_(ctx) (n)
      If(c2,p2,n2)
    }
    case Pack(implty:RawType,implterm:RawTerm, pubty:RawType) => {
      val implty_ = desugarty(ctx) (implty)
      val implterm_ = desugar_(ctx) (implterm)
      val pubty_ = desugarty(ctx) (pubty)
      Pack(implty_,implterm_,pubty_)
      }
    case Import(impl:RawTerm,pubty:RawTerm,pubterm:RawTerm,body:RawTerm) => (pubty,pubterm) match { 
      case (TyVarName(pubtystr),VarName(pubtermstr)) => {

      val impl_ = desugar_(ctx) (impl)
      val ctx2 = ctx + (pubtystr, TypeVarBinding(pubtystr))
      val ctx3 = ctx2+ (pubtermstr, NameBinding(pubtermstr))
      val body_ = desugar_(ctx3) (body)
      Unpack(impl_,pubtystr,pubtermstr,body_)
    }}
   
  }
}









